Nuprl Lemma : kind-rename_wf
11,40
postcript
pdf
ra
,
rt
:(Id
Id),
k
:Knd. kind-rename(
ra
;
rt
;
k
)
Knd
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
kind-rename(
ra
;
rt
;
k
)
,
x
.
t
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
x
(
s
)
,
x
(
s1
,
s2
)
Lemmas
kindcase
wf
,
Knd
wf
,
locl
wf
,
Id
wf
,
rcv
wf
,
IdLnk
wf
origin
ra, rt:(Id
Id), k:Knd. kind-rename(ra;rt;k) 
Knd ra, rt:(IdId), k:Knd. kind-rename(ra;rt;k) Knd x:A. B(x) T
x. t(x)x,y. t(x;y)